$\forall$${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} , $p$, ${\it p'}$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} . $p$($e$) $\Leftarrow\!\Rightarrow$ ${\it p'}$($e$))
\\[0ex]$\Rightarrow$ ($e_{2}$ = first $e$ $\geq$ $e_{1}$.$p$($e$) $\Leftarrow\!\Rightarrow$ $e_{2}$ = first $e$ $\geq$ $e_{1}$.${\it p'}$($e$))